Nuprl Lemma : R-da-Rlist
0,22
postcript
pdf
i
:Top,
L
:Top List. R-da(
(
L
);
i
) ~ reduce(
u
,
da
. R-da(
u
;
i
)
da
;;
L
)
latex
Definitions
es
realizer
ind
Rplus
compseq
tag
def
,
R-da(
R
;
i
)
,
(
L
)
,
es
realizer
ind
Rnone
compseq
tag
def
,
Top
,
t
T
,
type
List
,
x
:
A
B
(
x
)
,
s
~
t
,
x
:
A
.
B
(
x
)
Lemmas
top
wf
origin
i:Top, L:Top List. R-da(
(L);i) ~ reduce(
u,da. R-da(u;i) da;;L) i:Top, L:Top List. R-da((L);i) ~ reduce(u,da. R-da(u;i) da;;L) (L)
T
B(x)x:A. B(x)